Nuprl Lemma : refl_functionality_wrt_iff 13,42

T:Type, RR':(TT).
(xy:TR(x,y R'(x,y))  (Refl(T;x,y.R(x,y))  Refl(T;x,y.R'(x,y))) 
latex


Uprel 1, rel 1
DefinitionsP  Q, P  Q, P & Q, t  T, x(s1,s2), P  Q, x:AB(x),
Lemmasiff wf

origin